\begin{tabbing}
$\forall$${\it es}$:ES, ${\it Cmd}$:Type, ${\it In}$:AbsInterface(${\it Cmd}$), ${\it isupdate}$:(${\it Cmd}$$\rightarrow\mathbb{B}$), ${\it Sys}$, ${\it Out}$:AbsInterface(Top).
\\[0ex](E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ (E(${\it Out}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E(${\it In}$). ($\neg$($\uparrow$(${\it isupdate}$(${\it In}$($e$))))) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:sys{-}antecedent(${\it es}$;${\it Sys}$).\+
\\[0ex]($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$ $\in$ E) $\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]$\Rightarrow$ fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E(${\it In}$). $f$($e$) = $e$ $\in$ E)
\\[0ex]$\Rightarrow$ \=($\forall$${\it chain}$:(E(${\it Sys}$)$\rightarrow$(Id List)).\+
\\[0ex]chain{-}consistent($f$;${\it chain}$)
\\[0ex]$\Rightarrow$ \=($\forall$$a_{1}$, $a_{2}$:E(${\it Sys}$), $e_{1}$, $e_{2}$:E(${\it In}$).\+
\\[0ex]($\uparrow$(${\it isupdate}$(${\it In}$($e_{1}$))))
\\[0ex]$\Rightarrow$ ($\uparrow$(${\it isupdate}$(${\it In}$($e_{2}$))))
\\[0ex]$\Rightarrow$ $e_{1}$ is $f$$\ast$($a_{1}$)
\\[0ex]$\Rightarrow$ $e_{2}$ is $f$$\ast$($a_{2}$)
\\[0ex]$\Rightarrow$ ($a_{1}$ $<$loc $a_{2}$)
\\[0ex]$\Rightarrow$ ($\exists$$e$:E(${\it Sys}$). ($e$ $\leq$loc $e_{2}$  \& $e_{1}$ is $f$$\ast$($e$) \& $e$ is $f$$\ast$($a_{1}$))))))
\-\-\-
\end{tabbing}